diff options
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/calc.ML (renamed from spartan/core/congruence.ML) | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/spartan/core/congruence.ML b/spartan/core/calc.ML index d9f4ffa..67dc7fc 100644 --- a/spartan/core/congruence.ML +++ b/spartan/core/calc.ML @@ -1,6 +1,11 @@ -structure Congruence = struct +structure Calc = struct -(* Congruence context data *) +(* Calculational type context data + +A "calculational" type is a type expressing some congruence relation. In +particular, it has a notion of composition of terms that is often used to derive +proofs equationally. +*) structure RHS = Generic_Data ( type T = (term * indexname) Termtab.table @@ -17,23 +22,23 @@ fun register_rhs t var = RHS.map (Termtab.update (key, (t, idxname))) end -fun lookup_congruence ctxt t = +fun lookup_calc ctxt t = Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t) -(* Congruence declarations *) +(* Declaration *) local val Frees_to_Vars = map_aterms (fn tm => case tm of - Free (name, T) => Var (("*!"^name, 0), T) (*Hacky naming!*) + Free (name, T) => Var (("*!"^name, 0), T) (*FIXME: Hacky naming!*) | _ => tm) in -(*Declare the "right-hand side" of types that are congruences. - Does not handle bound variables, so no dependent RHS in declarations!*) -val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close> - "declare right hand side of congruence" +(*Declare the "right-hand side" of calculational types. Does not handle bound + variables, so no dependent RHS in declarations!*) +val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>calc\<close> + "declare right hand side of calculational type" (Parse.term -- (\<^keyword>\<open>rhs\<close> |-- Parse.term) >> (fn (t_str, rhs_str) => fn lthy => let @@ -47,7 +52,7 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close> end -(* Calculational reasoning: ".." setup *) +(* Ditto "''" setup *) fun last_rhs ctxt = map_aterms (fn t => case t of @@ -62,7 +67,7 @@ fun last_rhs ctxt = map_aterms (fn t => [prop] => (let val typ = Lib.type_of_typing (Logic.strip_assums_concl prop) - val (cong_pttrn, varname) = the (lookup_congruence ctxt typ) + val (cong_pttrn, varname) = the (lookup_calc ctxt typ) val unif_res = Pattern.unify (Context.Proof ctxt) (cong_pttrn, typ) Envir.init val rhs = #2 (the @@ -70,7 +75,7 @@ fun last_rhs ctxt = map_aterms (fn t => in rhs end handle Option => - error (".. can't match right-hand side of congruence")) + error (".. can't match right-hand side of calculational type")) | _ => Term.dummy) in rhs end | _ => t) |