From caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52 Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Tue, 7 Oct 2003 10:40:32 +0000 Subject: [PATCH] * removed currified constructors everywhere. A bug in the ocaml compiler allowed to use them, but the bug is now fixed so they cannot be used anymore. Sorry fellows, next time choose a better compiler ;-) --- helm/ocaml/cic_omdoc/cic2content.ml | 2 +- helm/ocaml/cic_omdoc/content2cic.ml | 4 +- helm/ocaml/cic_transformations/cexpr2pres.ml | 4 +- .../ocaml/cic_transformations/content2pres.ml | 100 ++++++++++-------- .../ocaml/mathql_generator/mQueryGenerator.ml | 59 +++++------ .../mathql_interpreter/mQueryInterpreter.ml | 34 +++--- .../mathql_interpreter/mQueryTParser.mly | 60 +++++------ helm/ocaml/mathql_interpreter/mQueryUtil.ml | 30 +++--- helm/ocaml/tactics/discriminationTactics.ml | 6 +- 9 files changed, 152 insertions(+), 147 deletions(-) diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml index 2c46c3c46..614848706 100644 --- a/helm/ocaml/cic_omdoc/cic2content.ml +++ b/helm/ocaml/cic_omdoc/cic2content.ml @@ -754,7 +754,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts = K.conclude_method = method_name; K.conclude_args = K.Aux (string_of_int no_constructors) - ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP)) + ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))) ::method_args@other_method_args; K.conclude_conclusion = try Some diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml index 65ea0d306..2cc72933b 100644 --- a/helm/ocaml/cic_omdoc/content2cic.ml +++ b/helm/ocaml/cic_omdoc/content2cic.ml @@ -154,8 +154,8 @@ let proof2cic deannotate p = conclude.Con.conclude_method = "Exists" || conclude.Con.conclude_method = "FalseInd") then (match (List.tl conclude.Con.conclude_args) with - Con.Term (C.AAppl - id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))::args -> + Con.Term (C.AAppl ( + id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))::args -> let subst = List.map (fun (u,t) -> (u, deannotate t)) exp_named_subst in let cargs = args2cic premise_env args in diff --git a/helm/ocaml/cic_transformations/cexpr2pres.ml b/helm/ocaml/cic_transformations/cexpr2pres.ml index f6a3b490d..0b303083d 100644 --- a/helm/ocaml/cic_transformations/cexpr2pres.ml +++ b/helm/ocaml/cic_transformations/cexpr2pres.ml @@ -145,7 +145,7 @@ let rec cexpr2pres ?(priority = 0) ?(assoc = false) ?(tail = []) t = let l' = List.map (function - None -> P.Mo [] "_" + None -> P.Mo([],"_") | Some t -> cexpr2pres t ) l in @@ -313,7 +313,7 @@ cexpr2pres_charcount ?(priority = 0) ?(assoc = false) ?(tail = []) t = let l' = List.map (function - None -> P.Mo [] "_" + None -> P.Mo([],"_") | Some t -> cexpr2pres t ) l in diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index 0fbd5e458..af3999a39 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -32,6 +32,16 @@ (* *) (***************************************************************************) +let p_mtr a b = Mpresentation.Mtr(a,b) +let p_mtd a b = Mpresentation.Mtd(a,b) +let p_mtable a b = Mpresentation.Mtable(a,b) +let p_mtext a b = Mpresentation.Mtext(a,b) +let p_mi a b = Mpresentation.Mi(a,b) +let p_mo a b = Mpresentation.Mo(a,b) +let p_mrow a b = Mpresentation.Mrow(a,b) +let p_mphantom a b = Mpresentation.Mphantom(a,b) + + let rec split n l = if n = 0 then [],l else let l1,l2 = @@ -400,8 +410,8 @@ and proof2pres term2pres p = | _ -> assert false) in (match conclude.Con.conclude_conclusion with None -> - P.Mrow [] - [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] + p_mrow [] + [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg] | Some c -> let conclusion = term2pres c in make_row [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] @@ -777,103 +787,103 @@ let content2pres term2pres (id,params,metasenv,obj) = let module P = Mpresentation in match obj with `Def (K.Const,thesis,`Proof p) -> - P.Mtable + p_mtable [None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"; None,"helm:xref","id"] - ([P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] + ([p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] ("UNFINISHED PROOF" ^ id ^"(" ^ String.concat " ; " (List.map UriManager.string_of_uri params)^ ")")])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "THESIS:"])] ; - P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mphantom [] - (P.Mtext [] "__") ; + p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] "THESIS:"])] ; + p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mphantom [] + (p_mtext [] "__") ; term2pres thesis])]] @ (match metasenv with None -> [] | Some metasenv' -> - [P.Mtr [] - [P.Mtd [] + [p_mtr [] + [p_mtd [] (* Conjectures are in their own table to make *) (* diffing the DOM trees easier. *) - (P.Mtable + (p_mtable [None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"] - ((P.Mtr [] - [P.Mtd [] - (P.Mrow [] - [P.Mtext [] "CONJECTURES:"])]):: + ((p_mtr [] + [p_mtd [] + (p_mrow [] + [p_mtext [] "CONJECTURES:"])]):: List.map (function (id,n,context,ty) -> - P.Mtr [] - [P.Mtd [] - (P.Mrow [Some "helm", "xref", id] + p_mtr [] + [p_mtd [] + (p_mrow [Some "helm", "xref", id] (List.map (function None -> - P.Mrow [] - [ P.Mi [] "_" ; - P.Mo [] ":?" ; - P.Mi [] "_"] + p_mrow [] + [ p_mi [] "_" ; + p_mo [] ":?" ; + p_mi [] "_"] | Some (`Declaration d) | Some (`Hypothesis d) -> let { K.dec_name = dec_name ; K.dec_type = ty } = d in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match dec_name with None -> "_" | Some n -> n) ; - P.Mo [] ":" ; + p_mo [] ":" ; term2pres ty] | Some (`Definition d) -> let { K.def_name = def_name ; K.def_term = bo } = d in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match def_name with None -> "_" | Some n -> n) ; - P.Mo [] ":=" ; + p_mo [] ":=" ; term2pres bo] | Some (`Proof p) -> let proof_name = p.K.proof_name in - P.Mrow [] - [ P.Mi [] + p_mrow [] + [ p_mi [] (match proof_name with None -> "_" | Some n -> n) ; - P.Mo [] ":=" ; + p_mo [] ":=" ; proof2pres term2pres p] ) (List.rev context) @ - [ P.Mo [] "|-" ] @ - [ P.Mi [] (string_of_int n) ; - P.Mo [] ":" ; + [ p_mo [] "|-" ] @ + [ p_mi [] (string_of_int n) ; + p_mo [] ":" ; term2pres ty ] )) ] ) metasenv' ))]] ) @ - [P.Mtr [] - [P.Mtd [] - (P.Mrow [] + [p_mtr [] + [p_mtd [] + (p_mrow [] [proof2pres term2pres p])]]) | _ -> raise ToDo ;; diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml index 40c0ea0b8..7e0dd9c96 100644 --- a/helm/ocaml/mathql_generator/mQueryGenerator.ml +++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml @@ -34,21 +34,18 @@ module U = MQGUtil let locate s = let query = - M.Property true M.RefineExact ["objectName"] [] [] [] [] - false (M.Const s) + M.Property (true,M.RefineExact,["objectName"],[],[],[],[],false,(M.Const s) ) in M.StatQuery query let unreferred target_pattern source_pattern = let query = - M.Bin M.BinFDiff + M.Bin (M.BinFDiff, ( - M.Property false M.RefineExact [] [] [] [] [] - true (M.Const target_pattern) - ) ( - M.Property false M.RefineExact ["refObj"] ["h:occurrence"] [] [] [] - true (M.Const source_pattern) + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const target_pattern)) + ), ( + M.Property(false,M.RefineExact,["refObj"],["h:occurrence"],[],[],[],true,(M.Const source_pattern)) - ) + )) in M.StatQuery query let compose cl = @@ -81,13 +78,11 @@ let compose cl = con "h:depth" (List.map U.string_of_depth d) in let property_must n c = - M.Property true M.RefineExact [n] [] - (cons false c) [] [] false (M.Const "") + M.Property(true,M.RefineExact,[n],[],(cons false c),[],[],false,(M.Const "")) in let property_only n cl = let cll = List.map (cons true) cl in - M.Property false M.RefineExact [n] [] - ! univ cll [] false (M.Proj None (M.AVar "obj")) + M.Property(false,M.RefineExact,[n],[],!univ,cll,[],false,(M.Proj(None,(M.AVar "obj")))) in let rec aux = function | [] -> () @@ -95,17 +90,17 @@ let compose cl = only := true; let l = List.map U.string_of_position l in univ := [(false, ["h:position"], set_val l)]; aux tail - | T.MustObj r p d :: tail -> + | T.MustObj(r,p,d) :: tail -> must := property_must "refObj" (r, [], p, d) :: ! must; aux tail - | T.MustSort s p d :: tail -> + | T.MustSort(s,p,d) :: tail -> must := property_must "refSort" ([], s, p, d) :: ! must; aux tail - | T.MustRel p d :: tail -> + | T.MustRel(p,d) :: tail -> must := property_must "refRel" ([], [], p, d) :: ! must; aux tail - | T.OnlyObj r p d :: tail -> + | T.OnlyObj(r,p,d) :: tail -> onlyobj := (r, [], p, d) :: ! onlyobj; aux tail - | T.OnlySort s p d :: tail -> + | T.OnlySort(s,p,d) :: tail -> onlysort := ([], s, p, d) :: ! onlysort; aux tail - | T.OnlyRel p d :: tail -> + | T.OnlyRel(p,d) :: tail -> onlyrel := ([], [], p, d) :: ! onlyrel; aux tail in let rec iter f g = function @@ -118,28 +113,28 @@ let compose cl = aux cl; let must_query = if ! must = [] then - M.Property false M.RefineExact [] [] [] [] [] true (M.Const ".*") + M.Property(false,M.RefineExact,[],[],[],[],[],true,(M.Const ".*")) else - iter (fun x -> x) (fun x y -> M.Bin M.BinFMeet x y) ! must + iter (fun x -> x) (fun x y -> M.Bin(M.BinFMeet,x,y)) ! must in - let onlyobj_val = M.Not (M.Proj None (property_only "refObj" ! onlyobj)) in - let onlysort_val = M.Not (M.Proj None (property_only "refSort" ! onlysort)) in - let onlyrel_val = M.Not (M.Proj None (property_only "refRel" ! onlyrel)) in + let onlyobj_val = M.Not (M.Proj(None,(property_only "refObj" ! onlyobj))) in + let onlysort_val = M.Not (M.Proj(None,(property_only "refSort" ! onlysort))) in + let onlyrel_val = M.Not (M.Proj(None,(property_only "refRel" ! onlyrel))) in let select_query x = match ! onlyobj, ! onlysort, ! onlyrel with | [], [], [] -> x - | _, [], [] -> M.Select "obj" x onlyobj_val - | [], _, [] -> M.Select "obj" x onlysort_val - | [], [], _ -> M.Select "obj" x onlyrel_val - | _, _, [] -> M.Select "obj" x (M.Test M.And onlyobj_val onlysort_val) - | _, [], _ -> M.Select "obj" x (M.Test M.And onlyobj_val onlyrel_val) - | [], _, _ -> M.Select "obj" x (M.Test M.And onlysort_val onlyrel_val) - | _, _, _ -> M.Select "obj" x (M.Test M.And (M.Test M.And onlyobj_val onlysort_val) onlyrel_val) + | _, [], [] -> M.Select("obj",x,onlyobj_val) + | [], _, [] -> M.Select("obj",x,onlysort_val) + | [], [], _ -> M.Select("obj",x,onlyrel_val) + | _, _, [] -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlysort_val))) + | _, [], _ -> M.Select("obj",x,(M.Test(M.And,onlyobj_val,onlyrel_val))) + | [], _, _ -> M.Select("obj",x,(M.Test(M.And,onlysort_val,onlyrel_val))) + | _, _, _ -> M.Select("obj",x,(M.Test(M.And,(M.Test(M.And,onlyobj_val,onlysort_val)),onlyrel_val))) in let letin_query = if ! letin = [] then fun x -> x else - let f (vvar, msval) x = M.LetVVar vvar msval x in + let f (vvar, msval) x = M.LetVVar(vvar,msval,x) in iter f (fun x y z -> x (y z)) ! letin in M.StatQuery (letin_query (select_query must_query)) diff --git a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml index 58fb7b87e..b2bfd445d 100644 --- a/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml +++ b/helm/ocaml/mathql_interpreter/mQueryInterpreter.ml @@ -64,7 +64,7 @@ let execute h x = | M.True -> U.mql_true | M.Const s -> [s] | M.Set l -> U.iter (eval_val c) l - | M.Test k y1 y2 -> + | M.Test (k,y1,y2) -> let cand y1 y2 = if eval_val c y1 = U.mql_false then U.mql_false else eval_val c y2 in @@ -89,16 +89,16 @@ let execute h x = | M.VVar i -> begin try List.assoc i c.vvars with Not_found -> warn (M.Subj (M.VVar i)); [] end - | M.Dot i p -> begin + | M.Dot (i,p) -> begin try List.assoc p (List.assoc i c.groups) - with Not_found -> warn (M.Subj (M.Dot i p)); [] end - | M.Proj None x -> List.map (fun (r, _) -> r) (eval_query c x) - | M.Proj (Some p) x -> + with Not_found -> warn (M.Subj (M.Dot (i,p))); [] end + | M.Proj (None,x) -> List.map (fun (r, _) -> r) (eval_query c x) + | M.Proj ((Some p),x) -> let proj_group_aux (q, v) = if q = p then v else [] in let proj_group a = U.iter proj_group_aux a in let proj_set (_, g) = U.iter proj_group g in U.iter proj_set (eval_query c x) - | M.Ex l y -> + | M.Ex (l,y) -> let rec ex_aux h = function | [] -> let d = {c with groups = h} in @@ -123,12 +123,12 @@ let execute h x = C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); r | M.Count y -> [string_of_int (List.length (eval_val c y))] - | M.Align s y -> U.iter (U.align s) (eval_val c y) + | M.Align (s,y) -> U.iter (U.align s) (eval_val c y) and eval_query c = function | M.Empty -> [] | M.Subj x -> List.map (fun s -> (s, [])) (eval_val c x) - | M.Log _ b x -> + | M.Log (_,b,x) -> if b then begin let t = P.start_time () in P.text_of_query (C.log h) x "\n"; @@ -145,10 +145,10 @@ let execute h x = C.log h (Printf.sprintf "Log: %s\n" r); s end - | M.If y x1 x2 -> + | M.If (y,x1,x2) -> if (eval_val c y) = U.mql_false then (eval_query c x2) else (eval_query c x1) - | M.Bin k x1 x2 -> + | M.Bin (k,x1,x2) -> let f = match k with | M.BinFJoin -> U.mql_union | M.BinFMeet -> U.mql_intersect @@ -161,13 +161,13 @@ let execute h x = | M.AVar i -> begin try [List.assoc i c.avars] with Not_found -> warn (M.AVar i); [] end - | M.LetSVar i x1 x2 -> + | M.LetSVar (i,x1,x2) -> let d = {c with svars = U.set (i, eval_query c x1) c.svars} in eval_query d x2 - | M.LetVVar i y x -> + | M.LetVVar (i,y,x) -> let d = {c with vvars = U.set (i, eval_val c y) c.vvars} in eval_query d x - | M.For k i x1 x2 -> + | M.For (k,i,x1,x2) -> let f = match k with | M.GenFJoin -> U.mql_union | M.GenFMeet -> U.mql_intersect @@ -179,11 +179,11 @@ let execute h x = f (eval_query d x2) (for_aux t) in for_aux (eval_query c x1) - | M.Add b z x -> + | M.Add (b,z,x) -> let f = if b then U.mql_prod else U.set_union in let g a s = (fst a, f (snd a) (eval_grp c z)) :: s in List.fold_right g (eval_query c x) [] - | M.Property q0 q1 q2 mc ct cfl el pat y -> + | M.Property (q0,q1,q2,mc,ct,cfl,el,pat,y) -> let subj, mct = if q0 then [], (pat, q2 @ mc, eval_val c y) else (q2 @ mc), (pat, [], eval_val c y) @@ -205,7 +205,7 @@ let execute h x = let s = P.stop_time t in C.log h (Printf.sprintf "Stat: %s,%i\n" s (List.length r)); r - | M.Select i x y -> + | M.Select (i,x,y) -> let rec select_aux = function | [] -> [] | h :: t -> @@ -214,7 +214,7 @@ let execute h x = then select_aux t else h :: select_aux t in select_aux (eval_query c x) - | M.Keep b l x -> + | M.Keep (b,l,x) -> let keep_path (p, v) t = if List.mem p l = b then t else (p, v) :: t in let keep_grp a = List.fold_right keep_path a [] in diff --git a/helm/ocaml/mathql_interpreter/mQueryTParser.mly b/helm/ocaml/mathql_interpreter/mQueryTParser.mly index 313636c80..2f8896185 100644 --- a/helm/ocaml/mathql_interpreter/mQueryTParser.mly +++ b/helm/ocaml/mathql_interpreter/mQueryTParser.mly @@ -47,31 +47,31 @@ | M.Const _ -> [] | M.VVar _ -> [] | M.Ex _ -> [] - | M.Dot rv _ -> [rv] + | M.Dot (rv,_) -> [rv] | M.Not x -> an_val x | M.StatVal x -> an_val x | M.Count x -> an_val x - | M.Align _ x -> an_val x - | M.Proj _ x -> an_set x - | M.Test _ x y -> iter an_val [x; y] + | M.Align (_,x) -> an_val x + | M.Proj (_,x) -> an_set x + | M.Test (_,x,y) -> iter an_val [x; y] | M.Set l -> iter an_val l and an_set = function | M.Empty -> [] | M.SVar _ -> [] | M.AVar _ -> [] | M.Subj x -> an_val x - | M.Keep _ _ x -> an_set x - | M.Log _ _ x -> an_set x + | M.Keep (_,_,x) -> an_set x + | M.Log (_,_,x) -> an_set x | M.StatQuery x -> an_set x - | M.Bin _ x y -> iter an_set [x; y] - | M.LetSVar _ x y -> iter an_set [x; y] - | M.For _ _ x y -> iter an_set [x; y] - | M.Add _ g x -> join (an_grp g) (an_set x) - | M.LetVVar _ x y -> join (an_val x) (an_set y) - | M.Select _ x y -> join (an_set x) (an_val y) - | M.Property _ _ _ _ c d _ _ x -> + | M.Bin (_,x,y) -> iter an_set [x; y] + | M.LetSVar (_,x,y) -> iter an_set [x; y] + | M.For (_,_,x,y) -> iter an_set [x; y] + | M.Add (_,g,x) -> join (an_grp g) (an_set x) + | M.LetVVar (_,x,y) -> join (an_val x) (an_set y) + | M.Select (_,x,y) -> join (an_set x) (an_val y) + | M.Property (_,_,_,_,c,d,_,_,x) -> join (an_val x) (iter an_con [c; List.concat d]) - | M.If x y z -> join (an_val x) (iter an_set [y; z]) + | M.If (x,y,z) -> join (an_val x) (iter an_set [y; z]) and fc (_, _, v) = an_val v and an_con c = iter fc c and fg (_, v) = an_val v @@ -241,18 +241,18 @@ | TRUE { M.True } | FALSE { M.False } | STR { M.Const $1 } - | avar FS path { M.Dot $1 $3 } + | avar FS path { M.Dot ($1,$3) } | vvar { M.VVar $1 } | LC vals RC { M.Set $2 } | LC RC { M.Set [] } | LP val_exp RP { $2 } | STAT val_exp { M.StatVal $2 } - | EX val_exp { M.Ex (analyze $2) $2 } + | EX val_exp { M.Ex ((analyze $2),$2) } | NOT val_exp { M.Not $2 } - | test_op { M.Test (f $1) (s $1) (t $1) } - | PROJ opt_path set_exp { M.Proj $2 $3 } + | test_op { M.Test ((f $1),(s $1),(t $1)) } + | PROJ opt_path set_exp { M.Proj ($2,$3) } | COUNT val_exp { M.Count $2 } - | ALIGN STR IN val_exp { M.Align $2 $4 } + | ALIGN STR IN val_exp { M.Align ($2,$4) } ; vals: | val_exp CM vals { $1 :: $3 } @@ -263,21 +263,21 @@ | LP set_exp RP { $2 } | svar { M.SVar $1 } | avar { M.AVar $1 } - | LET svar BE set_exp IN set_exp { M.LetSVar $2 $4 $6 } - | LET vvar BE val_exp IN set_exp { M.LetVVar $2 $4 $6 } + | LET svar BE set_exp IN set_exp { M.LetSVar ($2,$4,$6) } + | LET vvar BE val_exp IN set_exp { M.LetVVar ($2,$4,$6) } | FOR avar IN set_exp gen_op - { M.For (fst $5) $2 $4 (snd $5) } - | ADD distr grp_exp IN set_exp { M.Add $2 $3 $5 } - | IF val_exp THEN set_exp ELSE set_exp { M.If $2 $4 $6 } + { M.For ((fst $5),$2,$4,(snd $5)) } + | ADD distr grp_exp IN set_exp { M.Add ($2,$3,$5) } + | IF val_exp THEN set_exp ELSE set_exp { M.If ($2,$4,$6) } | PROP qualif mainc istrue isfalse attrc OF pattern val_exp - { M.Property (f $2) (s $2) (t $2) $3 $4 $5 $6 $8 $9 } - | LOG xml source set_exp { M.Log $2 $3 $4 } + { M.Property ((f $2),(s $2),(t $2),$3,$4,$5,$6,$8,$9) } + | LOG xml source set_exp { M.Log ($2,$3,$4) } | STAT set_exp { M.StatQuery $2 } - | KEEP allbut paths IN set_exp { M.Keep $2 $3 $5 } - | KEEP allbut IN set_exp { M.Keep $2 [] $4 } + | KEEP allbut paths IN set_exp { M.Keep ($2,$3,$5) } + | KEEP allbut IN set_exp { M.Keep ($2,[],$4) } | bin_op - { M.Bin (f $1) (s $1) (t $1) } - | SELECT avar FROM set_exp WHERE val_exp { M.Select $2 $4 $6 } + { M.Bin ((f $1),(s $1),(t $1)) } + | SELECT avar FROM set_exp WHERE val_exp { M.Select ($2,$4,$6) } | SUBJ val_exp { M.Subj $2 } ; query: diff --git a/helm/ocaml/mathql_interpreter/mQueryUtil.ml b/helm/ocaml/mathql_interpreter/mQueryUtil.ml index 30e6688ee..4484c486b 100644 --- a/helm/ocaml/mathql_interpreter/mQueryUtil.ml +++ b/helm/ocaml/mathql_interpreter/mQueryUtil.ml @@ -116,41 +116,41 @@ let text_of_query out x sep = | M.Const s -> txt_str out s | M.Set l -> txt_val_list l | M.VVar vv -> txt_vvar vv - | M.Dot av p -> txt_avar av; out "."; txt_path out p - | M.Proj op x -> out "proj "; txt_opt_path op; txt_set x - | M.Ex b x -> out "ex "; txt_val x + | M.Dot (av,p) -> txt_avar av; out "."; txt_path out p + | M.Proj (op,x) -> out "proj "; txt_opt_path op; txt_set x + | M.Ex (b,x) -> out "ex "; txt_val x (* | M.Ex b x -> out "ex ["; txt_list out txt_avar "," b; out "] "; txt_val x *) | M.Not x -> out "not "; txt_val x - | M.Test k x y -> out "("; txt_val x; txt_test k; txt_val y; out ")" + | M.Test (k,x,y) -> out "("; txt_val x; txt_test k; txt_val y; out ")" | M.StatVal x -> out "stat "; txt_val x | M.Count x -> out "count "; txt_val x - | M.Align s x -> out "align "; txt_str out s; out " in "; txt_val x + | M.Align (s,x) -> out "align "; txt_str out s; out " in "; txt_val x and txt_set = function | M.Empty -> out "empty" | M.SVar sv -> txt_svar sv | M.AVar av -> txt_avar av - | M.Property q0 q1 q2 mc ct cfl xl b x -> + | M.Property (q0,q1,q2,mc,ct,cfl,xl,b,x) -> out "property "; txt_qualif q0 q1 q2; main mc; txt_istrue ct; txt_list out txt_isfalse "" cfl; txt_exp_list xl; out " of "; pattern b; txt_val x - | M.Bin k x y -> out "("; txt_set x; txt_bin k; txt_set y; + | M.Bin (k,x,y) -> out "("; txt_set x; txt_bin k; txt_set y; out ")" - | M.LetSVar sv x y -> out "let "; txt_svar sv; out " be "; + | M.LetSVar (sv,x,y) -> out "let "; txt_svar sv; out " be "; txt_set x; out " in "; txt_set y - | M.LetVVar vv x y -> out "let "; txt_vvar vv; out " be "; + | M.LetVVar (vv,x,y) -> out "let "; txt_vvar vv; out " be "; txt_val x; out " in "; txt_set y - | M.Select av x y -> out "select "; txt_avar av; out " from "; + | M.Select (av,x,y) -> out "select "; txt_avar av; out " from "; txt_set x; out " where "; txt_val y | M.Subj x -> out "subj "; txt_val x - | M.For k av x y -> out "for "; txt_avar av; out " in "; + | M.For (k,av,x,y) -> out "for "; txt_avar av; out " in "; txt_set x; txt_gen k; txt_set y - | M.If x y z -> out "if "; txt_val x; out " then "; + | M.If (x,y,z) -> out "if "; txt_val x; out " then "; txt_set y; out " else "; txt_set z - | M.Add d g x -> out "add "; txt_distr d; txt_grp g; + | M.Add (d,g,x) -> out "add "; txt_distr d; txt_grp g; out " in "; txt_set x - | M.Log a b x -> out "log "; txt_log a b; txt_set x + | M.Log (a,b,x) -> out "log "; txt_log a b; txt_set x | M.StatQuery x -> out "stat "; txt_set x - | M.Keep b l x -> out "keep "; txt_allbut b; txt_path_list l; + | M.Keep (b,l,x) -> out "keep "; txt_allbut b; txt_path_list l; txt_set x in txt_set x; out sep diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index 4a349e54c..c413d4694 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -275,8 +275,8 @@ prerr_endline ("XXXX nth funzionano ") ; C.Lambda (binder,source,(aux target (k+1))) | _ -> if (id = false_constr_id) - then (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 []) - else (C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/True.ind") 0 []) + then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[])) + else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[])) in aux red_ty 1 ) constructor_list @@ -285,7 +285,7 @@ prerr_endline ("XXXX nth funzionano ") ; let (proof',goals') = EliminationTactics.elim_type_tac - ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ) + ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[])) ~status in (match goals' with -- 2.39.2