TFL/tfl.sml
changeset 7052 4c201f27c74e
parent 6566 7ed743d18af7
child 7262 a05dc63ca29b
equal deleted inserted replaced
7051:9b6bdced3dc6 7052:4c201f27c74e
   289  end;
   289  end;
   290 
   290 
   291 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
   291 local fun mk_functional_err s = raise TFL_ERR{func = "mk_functional", mesg=s}
   292       fun single [Free(a,_)] = 
   292       fun single [Free(a,_)] = 
   293 	      mk_functional_err (a ^ " has not been declared as a constant")
   293 	      mk_functional_err (a ^ " has not been declared as a constant")
   294         | single [f] = f
   294         | single [_$_] = 
       
   295 	      mk_functional_err "recdef does not allow currying"
       
   296         | single [Const arg] = arg
       
   297 	| single [_] = mk_functional_err "recdef: bad function name"
   295         | single fs  = mk_functional_err (Int.toString (length fs) ^ 
   298         | single fs  = mk_functional_err (Int.toString (length fs) ^ 
   296                                           " distinct function names!")
   299                                           " distinct function names!")
   297 in
   300 in
   298 fun mk_functional thy clauses =
   301 fun mk_functional thy clauses =
   299  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
   302  let val (L,R) = ListPair.unzip (map HOLogic.dest_eq clauses)
   300                    handle _ => raise TFL_ERR
   303                    handle _ => raise TFL_ERR
   301 		       {func = "mk_functional", 
   304 		       {func = "mk_functional", 
   302 			mesg = "recursion equations must use the = relation"}
   305 			mesg = "recursion equations must use the = relation"}
   303      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   306      val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
   304      val fcon as Const (fname, ftype) = single (gen_distinct (op aconv) funcs)
   307      val (fname, ftype) = single (gen_distinct (op aconv) funcs)
   305      val dummy = map (no_repeat_vars thy) pats
   308      val dummy = map (no_repeat_vars thy) pats
   306      val rows = ListPair.zip (map (fn x => ([],[x])) pats,
   309      val rows = ListPair.zip (map (fn x => ([],[x])) pats,
   307                               map GIVEN (enumerate R))
   310                               map GIVEN (enumerate R))
   308      val names = foldr add_term_names (R,[])
   311      val names = foldr add_term_names (R,[])
   309      val atype = type_of(hd pats)
   312      val atype = type_of(hd pats)
   322      val dummy = case (originals\\finals)
   325      val dummy = case (originals\\finals)
   323              of [] => ()
   326              of [] => ()
   324           | L => mk_functional_err("The following rows (counting from zero)\
   327           | L => mk_functional_err("The following rows (counting from zero)\
   325                                    \ are inaccessible: "^stringize L)
   328                                    \ are inaccessible: "^stringize L)
   326  in {functional = Abs(Sign.base_name fname, ftype,
   329  in {functional = Abs(Sign.base_name fname, ftype,
   327 		      abstract_over (fcon, 
   330 		      abstract_over (Const(fname,ftype), 
   328 				     absfree(aname,atype, case_tm))),
   331 				     absfree(aname, atype, case_tm))),
   329      pats = patts2}
   332      pats = patts2}
   330 end end;
   333 end end;
   331 
   334 
   332 
   335 
   333 (*----------------------------------------------------------------------------
   336 (*----------------------------------------------------------------------------