X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=b194fbfa9fd9f5afce2bfa3f6384ec6d660ab85c;hb=0b76904a3f10bfd6390d26172fd6979626bd72f4;hp=b0820f225af0ad2da3468359d29c03816a2136e2;hpb=8eff703769b4ed115d71817d4c0c9628de5295a7;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index b0820f225..b194fbfa9 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -54,20 +54,24 @@ let list_init f i = (****************************************************************************) -type flavour = Cic.object_flavour +type flavour = C.object_flavour type name = string option type hyp = string -type what = Cic.annterm +type what = C.annterm type how = bool -type using = Cic.annterm +type using = C.annterm type count = int type note = string type where = (hyp * name) option -type inferred = Cic.annterm -type pattern = Cic.annterm +type inferred = C.annterm +type pattern = C.annterm +type body = C.annterm option +type types = C.anninductiveType list +type lpsno = int type step = Note of note - | Theorem of flavour * name * what * note + | Inductive of types * lpsno * note + | Statement of flavour * name * what * body * note | Qed of note | Id of note | Intros of count option * name list * note @@ -83,7 +87,34 @@ type step = Note of note (* annterm constructors *****************************************************) -let mk_arel i b = Cic.ARel ("", "", i, b) +let mk_arel i b = C.ARel ("", "", i, b) + +(* FG: this is really awful !! *) +let arel_of_name = function + | C.Name s -> mk_arel 0 s + | C.Anonymous -> mk_arel 0 "_" + +(* helper functions on left params for use with inductive types *************) + +let strip_lps lpsno arity = + let rec aux no lps = function + | C.AProd (_, name, w, t) when no > 0 -> + let lp = name, Some w in + aux (pred no) (lp :: lps) t + | t -> lps, t + in + aux lpsno [] arity + +let merge_lps lps1 lps2 = + let map (n1, w1) (n2, _) = + let n = match n1, n2 with + | C.Name _, _ -> n1 + | _ -> n2 + in + n, w1 + in + if lps1 = [] then lps2 else + List.map2 map lps1 lps2 (* grafite ast constructors *************************************************) @@ -100,9 +131,25 @@ let mk_notenote str a = let mk_thnote str a = if str = "" then a else mk_note "" :: mk_note str :: a -let mk_theorem flavour name t = +let mk_inductive types lpsno = + let map1 (lps1, cons) (name, arity) = + let lps2, arity = strip_lps lpsno arity in + merge_lps lps1 lps2, (name, arity) :: cons + in + let map2 (lps1, types) (_, name, kind, arity, cons) = + let lps2, arity = strip_lps lpsno arity in + let lps1, rev_cons = List.fold_left map1 (lps1, []) cons in + merge_lps lps1 lps2, (name, kind, arity, List.rev rev_cons) :: types + in + let map3 (name, xw) = arel_of_name name, xw in + let rev_lps, rev_types = List.fold_left map2 ([], []) types in + let lpars, types = List.rev_map map3 rev_lps, List.rev rev_types in + let obj = N.Inductive (lpars, types) in + G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) + +let mk_statement flavour name t v = let name = match name with Some name -> name | None -> assert false in - let obj = N.Theorem (flavour, name, t, None) in + let obj = N.Theorem (flavour, name, t, v) in G.Executable (floc, G.Command (floc, G.Obj (floc, obj))) let mk_qed = @@ -182,22 +229,23 @@ let mk_vb = G.Shift floc (* rendering ****************************************************************) let rec render_step sep a = function - | Note s -> mk_notenote s a - | Theorem (f, n, t, s) -> mk_theorem f n t :: mk_thnote s a - | Qed s -> mk_qed :: mk_tacnote s a - | Id s -> mk_id sep :: mk_tacnote s a - | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a - | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a - | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a - | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a - | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a - | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a - | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a - | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a - | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a - | Branch ([], s) -> a - | Branch ([ps], s) -> render_steps sep a ps - | Branch (ps :: pss, s) -> + | Note s -> mk_notenote s a + | Statement (f, n, t, v, s) -> mk_statement f n t v :: mk_thnote s a + | Inductive (lps, ts, s) -> mk_inductive lps ts :: mk_thnote s a + | Qed s -> mk_qed :: mk_tacnote s a + | Id s -> mk_id sep :: mk_tacnote s a + | Intros (c, ns, s) -> mk_intros c ns sep :: mk_tacnote s a + | Cut (n, t, s) -> mk_cut n t sep :: mk_tacnote s a + | LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a + | Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a + | Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a + | Apply (t, s) -> mk_apply t sep :: mk_tacnote s a + | Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a + | Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a + | ClearBody (n, s) -> mk_clearbody n sep :: mk_tacnote s a + | Branch ([], s) -> a + | Branch ([ps], s) -> render_steps sep a ps + | Branch (ps :: pss, s) -> let a = mk_ob :: mk_tacnote s a in let a = List.fold_left (render_steps mk_vb) a (List.rev pss) in mk_punctation sep :: render_steps mk_cb a ps @@ -218,7 +266,7 @@ let render_steps a = render_steps mk_dot a let rec count_step a = function | Note _ - | Theorem _ + | Statement _ | Qed _ -> a | Branch (pps, _) -> List.fold_left count_steps a pps | _ -> succ a @@ -227,7 +275,8 @@ and count_steps a = List.fold_left count_step a let rec count_node a = function | Note _ - | Theorem _ + | Inductive _ + | Statement _ | Qed _ | Id _ | Intros _